$\forall$${\it es}$:ES, $e$:E, $l$:IdLnk, $L$:E List. rcvs from $e$ on $l$ = $L$ $\Rightarrow$ ($\forall$$i$:$\mathbb{N}$$_{\mbox{\scriptsize $<\parallel$$L$$\parallel$}}$. index($L$[$i$]) $=$ $i$ $\in$ $\mathbb{Z}$)